PR summary 7ab71b05d7

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 7ab71b0).

• +0 new declarations
• −0 removed declarations

No declaration differences.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 7ab71b05d7
Reference commit 9c27dca6e4

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Also reverts #34391

I think the reason for this PR still applies; we shouldn't ungeneralize the lemmas about the general definitions in core. This might mean having separate Sort and Type sections, or it might mean making an RFC to ungeneralize them upstream.

because Pi.hasLe doesn't support sorts, see this thread.

Please add the explanation in the commit message above the fold; GitHub discuseions are hard to find in large PRs

Moved that sentence above the fold.

GitHub discussions are hard to find in large PRs

(link)
(edit: see also small Zulip remark)

Oh, I thought you had a reason to justify why it didn't support sorts

🚀 Pull request has been placed on the maintainer queue by joneugster.

I'd like to hear from @b-mehta here before reverting his PR

(the long PR title is perhaps good evidence that this PR is doing two unrelated things that would happen in separate PRs)

I don't think the universe ungeneralisation is a good idea, and it's not clear to me that it's motivated. It looks like exactly one lemma doesn't work with the generalised universes, but that doesn't motivate making a whole series of true lemmas unusable. Can't we just change map_mono to take {α β : Type*} instead?

exactly one lemma

See #30526, it's the entire file, I changed just map_mono here as a proof-of-concept since it has a TODO comment.
But regardless, I prefer to postpone this discussion to #30526 if the move itself is good to go, so I reverted the changes to Logic/Relation.lean.

(btw my comment above reads a bit snarky to me but I'm not sure how to phrase it better, no snarky-ness intended)

Letting LE accept Sort will solve the universe issues, do you think core will be okay with such a change?

Letting LE accept Sort will solve the universe issues, do you think core will be okay with such a change?

I think the first half of this question is a good one for Zulip; in particular, this is needed for allow f ≤ g when f g : \forall x ≤ 3, Nat.

It sounds like the motivation is also that there are other core defs which already are generalized to Sort

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job